\documentclass[12pt]{gatech-thesis}
\usepackage{amsmath,amsfonts,amssymb,latexsym,float,epsfig,subfigure,mathtools}
\usepackage{gatech-thesis-index}

%%
%% This example is adapted from ucthesis.tex, a part of the
%% UCTHESIS class package...
%%
\title{A Java Library for $\pi$-Calculus \\
based applications} %% If you want to specify a linebreak
                               %% in the thesis title, you MUST use
                               %% \protect\\ instead of \\, as \\ is a
                               %% fragile command that \MakeUpperCase
                               %% will break!
\author{Prajyoti Waghmare}
\department{Indian Institute of Technology, Kanpur}


%% Can have up to six readers, plus principaladvisor and
%% committeechair. All have the form
%%
%%  \reader{Name}[Department][Institution]
%%
%% The second and third arguments are optional, but if you wish to
%% supply the third, you must supply the second. Department defaults
%% to the department defined above and Institution defaults to Georgia
%% Institute of Technology.

\principaladvisor{Professor Satyadev Nandakumar}
%\committeechair{Professor Ignatius Arrogant}
%\firstreader{Professor General Reference}
%\secondreader{Professor Ivory Insular}%[Department of Computer Science and Operations Research][North Dakota State University]
%\thirdreader{Professor Earl Grey}
%\fourthreader{Professor John Smith}
%\fifthreader{Professor Jane Doe}%[Another Department With a Long Name][Another Institution]
%\setcounter{secnumdepth}{2}
\degree{Masters in Computer Science and Engineering}

%% Set \listmajortrue below, then uncomment and set this for
%% interdisciplinary PhD programs so that the title page says
%% ``[degree] in [major]'' and puts the department at the bottom of
%% the page, rather than saying ``[degree] in the [department]''

%% \major{Algorithms, Combinatorics, and Optimization} 

\copyrightyear{2013}
\submitdate{March 2013} % Must be the month and year of graduation,
                         % not thesis approval! As of 2010, this means
                         % this text must be May, August, or December
                         % followed by the year.

%% The date the last committee member signs the thesis form. Printed
%% on the approval page.
%\approveddate{1 July 2010}

\bibfiles{javapi}

%% The following are the defaults
%%    \titlepagetrue
%%    \signaturepagetrue
%%    \copyrightfalse
\figurespagefalse
\tablespagefalse
%%    \contentspagetrue
%%    \dedicationheadingfalse
\bibpagetrue
\indexpagetrue
%%    \thesisproposalfalse
%%    \strictmarginstrue
%%    \dissertationfalse
%%    \listmajorfalse
%%    \multivolumefalse

\begin{document}
\bibliographystyle{gatech-thesis}
%%
\begin{preliminary}
%% \begin{dedication}
%% \null\vfil
%% {\large
%% \begin{center}
%% To myself,\\\vspace{12pt}
%% Perry H. Disdainful,\\\vspace{12pt}
%% the only person worthy of my company.
%% \end{center}}
%% \vfil\null
%% \end{dedication}
%% \begin{preface}
%% Theses have elements.  Isn't that nice?
%% \end{preface}
\begin{acknowledgements}
I want to ``thank'' my committee, without whose ridiculous demands, I
would have graduated so, so, very much faster.
\end{acknowledgements}
\begin{abstract}
  Process Calculi is a family of approaches widely used for modelling concurrent environments. Concurrency makes it essential to handle high-level tasks of interaction, communication and synchronization between collection of processes. $\pi$-calculus has been recently added to this family by Robin Milner, Jaochim Parrow and David Walker. Several attempts have been made for modelling a programming framework for $pi$-calculus. Pict$^3$ a programming language based on $\pi$-calculus is one such attempt. \\
This thesis aims to create a programming framework in Java which is easy to use and does not require any new language to be learnt. The library thus created models mobile channels and concurrent interactions between processes using channels. In the later part of the thesis we present formal semantics to prove the type safety and type soundness of the programs written using this library. 
  %% This is the abstract that must be turned in as hard copy to the
  %% thesis office to meet the UMI requirements. It should \emph{not} be
  %% included when submitting your ETD. Comment out the abstract
  %% environment before submitting. It is recommended that you simply
  %% copy and paste the text you put in the summary environment into this
  %% environment. The title, your name, the page count, and your
  %% advisor's name will all be generated automatically.
\end{abstract}
% print table of contents, figures and tables here.
\contents
% if you need a "List of Symbols or Abbreviations" look into
% gatech-thesis-gloss.sty.

%% \begin{summary}
%% Why should I provide a summary?  Just read the thesis.
%% \end{summary}
\end{preliminary}
\chapter{Introduction}
\section{Motivation}
$\pi$ calculus is a simple yet expressive calculus developed by Robin Milner, Jaochim Parrow and David Walker for modelling and studying the interaction of concurrent processes. The basic $\pi$-calculus has been extended in various directions like Locality-Aware extension$^1$, Stochastic $\pi$-calculus$^2$, embedded systems and various others. Also spi calculus and applied pi have been found to be successful in reasoning about cryptographic protocols. With growing number of applications, there arises a need to formalize $\pi$-calculus in a programming language for practical use. Pict$^4$ is one such attempt which is a full blown language dedicated to handle $\pi$-calculus constructs. PiLib is a libary written in SCALA$^5$. \\
Concurrency handling in commonly used languages like Java and C++ makes it extremely slow and hence researchers have not considered them. However, this thesis aims at developing a Java library for pi calculus. In order to tackle the concurrency problem, software transactional memory is used which has been experimentally proved to be faster than the use of the usual synchronized keyword in Java.%%Citation for deuce.
Another motivation for the use of deuce library was that it is extremely easy to use and keeps the code clean. 

\section{Contribution}
This thesis contributes a Java library which provides an API for using $\pi$-calculus functions. The later part of the thesis also provides the proof for type safety of the JAVA language along with this library. Concurrency control is handled using Deuce STM which is a open source java support for software transactional memory. The $\pi$-calculus notions of channels and processes are modelled as \'Classes\' in Java which can interact as defined in the formal definition of $\pi$-calculus by Robin Milner.%%citation of book 
The later part of this document included a proof of the type safety and type soundness of the programs written using this library.  

\section{Structure}
\begin{enumerate}
\item $\pi$ calculus
\item Stm
\item library routines
\item type safety and soundness
\item Conclusion
\item Related Work
\end{enumerate}

%% \subsection{Secondary Concept}

%% This is the secondary concept.

%% \subsubsection{Even more secondary}

%% This is really not all that important.

%% \begin{table}
%% \caption{A table, centered.}
%% \begin{center}
%% \begin{tabular}{|l|r|}
%%   \hline 
%% Title & Author \\
%% \hline
%% War And Peace & Leo Tolstoy \\
%% The Great Gatsby & F. Scott Fitzgerald \\ \hline
%% \end{tabular}
%% \end{center}
%% \end{table}
%%
\chapter{Previous Work}
4 describes Pict, a strongly-typed concurrent programming language constructed in terms of an explicitly-typed $\pi$ calculus core language. \\
Stochastic Pi Machine(SPim) is a programming language for designing and simulating computer models of biological processes. The mathematics behind the language is based on pi calculus whereas the algorithm utilizes principles of physical chemistry. 
\chapter{Background}
\section{$\pi$-calculus}
\subsection{History of $\pi$-Calculus}
The $\lambda$ calculus is restricted to formulating the notion of sequential interaction in a clean mathematical and formal way. The technological advances has brought a significant change in computing practice giving rise to interactive systems. People, computers and softwares utilize mobility continuously. Thus $\pi$ calculus was developed in the late 1980s in order to express mobile systems accurately. Thus the $\pi$-calculus is a more complete way of formalizing real world systems, than $\lambda$ calculus, in which the elements alter as they interact. \\
The basic CCS(Concurrent Communication Systems) includes channels and processes where names can be transferred via channels from one process to other. $\pi$-calculus made an addition by adding mobility of channels i.e trasferring channels from one process to other process. Thus the connectivity of the system can change dynamically. The $\pi$-calculus uses the notion of mobility of channels because it can successfully model the movement of processes.% and it is simple.
\subsection{{\bf $\pi$} Calculus Operations}
\begin{itemize}
  \item {\it Empty Process (0)} : The process which cannot perform any actions
  \item {\it Input Process (a(x).P)} : A name is recieved along the channel {\bf a} and the variable/channel {\bf x} is bound to this value and then acts as P
  \item {\it Output Process ($\bar{a}<x>$.P)} : The value {\bf x} is sent along the channel {\bf a} and then acts as P
  \item {\it Scope (({\it v}x)P}) : This limits the scope of {\bf x} to P only
  \item {\it Choice Operator (P+Q)} : The agent chooses non-deterministically to proceed as process P or process Q
  \item {\it Parallel Composition (P$|$Q)} : The two processes P and Q proceed simultaneously 
  \item {\it Replication (!P)} : Denotes infinite number of copies of P, all running in parallel
\end{itemize}

\subsection{An Example}
Consider a system where we have multiple Cars each connected to a transmitter. The motion of the Car is determined by the transmitter. All the transmitters are connected to each other(figure 1). At some point a transmitter T1 can transfer the channel connecting itself with Car C1 to some other transmitter T2. This is called mobility of Channel. This will lead to change in the connectivity of the system. 
\begin{figure}
\caption{Initial Stage}
\includegraphics[width=130mm, height = 60mm]{figures/carTrans1.png}
\end{figure}
\begin{figure}
\caption{After tranmission of a Channel}
\includegraphics[width=130mm, height = 60mm]{figures/carTrans2.png}
\end{figure}
In order to study the mobility of one channel from one transmitter to another let us consider the following system with two transmitters and one Car and one channel.(figure 3) 
\begin{figure}
\caption{Focussed view}
\includegraphics[width=80mm, height = 60mm]{figures/carTrans3.png}
\includegraphics[width=80mm, height = 60mm]{figures/carTrans4.png}
\end{figure}
%% \begin{figure}
%% \caption{After Transferring Channel}
%% \includegraphics[width=130mm, height = 60mm]{figures/carTrans4.png}
%% \end{figure}

\chapter{Type Soundness Proof}
\section{Introduction}
The extent to which a programming language restricts the syntax so as to prevent type errors is called type safety. Robin Milner correctly stated type safety as "Well typed programs cannot go wrong!''
JavaPict is an extension to Java, which adds two new notions, of processes and channels. The environment consists of processes and channels, wherein processes are entities which holds ports wherein the channels are attached. For simplicity we avoid the model of sending channels over channels. Channels are synchronous objects through which processes send and receive messages from other connected processes. \\
This part of the thesis proves that JavaPict is type sound. Formally we use Featherweight generic Java and extend it to include channels and prove the type soundness of the new system.
\section{Featherweight Java (FJ)}
\subsection{Background}
Featherweight java or FJ is a new contender for a minimal core calculus for modelling Java's type system. FJ is designed, giving more importance to compactness than to completeness. There are only five forms of expressions in FJ namely, object creation, method invocation, field access, casting, and variables. FJ was designed to model languages that extend Java a and making . 
\subsection{Featherweight Java(FJ) definition}
A java program consists of class definitions and  an expression. Formally, a Java program is a pair of class table (CT) and an expression i.e. (CT, e). A class table is a mapping from class names C to class declarations L. Certain restrictions are imposed in order to maintain syntactic regularity. 
\begin{itemize}
\item Class
  \begin{itemize}
    \item Every class has a superclass i.e the definition should include an {\it extends} clause i.e class C extends D \{...\} (In trivial case, the superclass is {\it Object})
    \item The class {\it Object} is not included in the class table
    \item Class always contains one constructor with number of arguments equal to the sum of number of its own fields and the number of fields in superclass. 
    \item All fields are public and final 
    \item Class contains methods denoted by ${\overline M}$
  \end{itemize}
\item Method
  \begin{itemize}
    \item A method header contains a return type, a method name and arguments  
    \item Method includes only a single expression containing a return statement
  \end{itemize}
\end{itemize}
FJ defines some rules to maintain syntactic regularity. Class declaration always includes the supertype even if it is Object. The class definition must include a constructor where number of parameters equal to the number of fields. We should always (1) include the supertype(even if it is Object), (2) write out the constructor (even when these are trivial classes like A and B given below).  Consider the following class definitions in FJ,
\begin{verbatim}
class A extends Object {
     A() { super(); }
}
class B extends Object {
     B() { super(); }
}
class Pair extends Object {
     Object fst;
     Object snd;
     Pair(Object fst, Object snd){
          Pair(Objct fst, Object snd){
             super(); this.fst = fst; this.snd = snd;
          }
     }
     Pair setfst(Object fst){
          return new Pair(fst, this.snd);
     }
}
\end{verbatim}
\section{Featherweight Generic Java (FGJ)}
\section{Extension to FGJ}
\section{Type soundness proof}

\chapter{Conclusion}

\nocite{*}
%% We need this since this file doesn't ACTUALLY \cite anything...
%%
\appendix
\chapter{Some Ancillary Stuff}

Ancillary material should be put in appendices, which 
appear just before the bibliography. 

\begin{postliminary}
\references
\postfacesection{Index}{%
%%             ... generate an index here
%%         look into gatech-thesis-index.sty
}
\begin{vita}
Perry H. Disdainful was born in an insignificant town
whose only claim to fame is that it produced such a fine
specimen of a researcher.
\end{vita}
%%%%\gtindex
\end{postliminary}

\end{document}
%% \documentclass[11pt,twopage,oneandahalfspaced,normalmargins]{gatech-thesis}
%% \usepackage{amsmath,amssymb,latexsym,float,epsfig,subfigure}

%% \title{A Java Library for \pi-calculus \\ based implementations}
%% \author{Prajyoti Waghmare}
%% \principaladviser{Dr. Satyadev Nandakumar}
%% \begin{document}
%% \begin{itemize}
%% \item hello
%% \end{itemize}
%% \author{Prajyoti Waghmare}
%% \begin{abstract}

%% \end{abstract}

%% \end{document}
